es:ES, L:(Id List).
fischer(L)
 (e:E. (loc(e)  L)  ("x" changed before e)  fEvent((last change to "x" before e))) 

latex

Definitions	, t  T, A c B, fEvent(e), P  Q, x:A. B(x), True, T, Id, A, fischer(L), P & Q, False, @e(xv)
Lemmas	event system wf, fischer wf, es-E wf, Id wf, l member wf, es-loc wf, es-dtype wf, deq wf, subtype rel self, changed wf, assert wf, loc-last-change, true wf, squash wf, last-change-property